\documentclass{beamer}
\usepackage[T2A]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[english,russian]{babel}
\usepackage{xcolor}           		% задаем цвета
\usepackage{cite,enumerate,float,indentfirst}
\usepackage{amssymb,amsfonts,amsmath,mathtext}
\usepackage{graphicx}
\usepackage{epsfig,float}     		% вставлять рисунки
\usepackage{psfrag}           		% редактировать надписи на рисунках
\graphicspath{{images/}} %путь к рисункам

% Стилевой файл
\usetheme{CambridgeUS}
%\usecolortheme{beaver}
\usecolortheme{whale}
% Название
\title[Исследование систем типизированного $\lambda$-исчисления]{{\huge Реализация и исследование систем типизированного $\lambda$-исчисления 
с контролем изменений наиболее общего типа}}
\author{Курьян К.П.}
\institute{Санкт-Петербургский Академический университет РАН}
\date{}

\begin{document}

%%титульная страница
\begin{frame}

% университет
  \parbox[c]{0.15\textwidth}{
     \includegraphics[width=0.15\textwidth]{AU} %левый логотип
  }
  \parbox[c]{0.8\textwidth}{
     \begin{center}
       Санкт-Петербургский Академический университет РАН \\ Кафедра математических и информационных технологий
     \end{center}
  }

  \vspace{1em}
  \begin{center}
   {\LARGE Реализация и исследование систем типизированного $\lambda$-исчисления с контролем изменений наиболее общего типа}
  \end{center}   
  \begin{center}
   К.П. Курьян
  \end{center} 
  \vspace{1em}
  \begin{center}
   \parbox[c]{0.7\textwidth}{
     Научный руководитель: \hfill Д. Н. Москвин
   }
  \end{center}
\end{frame}

\section{Теория}
\subsection{Введение в $\lambda$-исчисление}
\begin{frame}
  \begin{block}{}
  В $\lambda$ -исчислении две операции: применение и абстракция.
  \begin{description}
  \item[Применение (Application):] \hspace*{\fill} \\
  F X \\  
  С точки зрения программиста: \\
  F (алгоритм) применяется к X (входные данные).  \\
   \\
  \item[Абстракция (Abstraction):] \hspace*{\fill} \\
  Пусть M = M[x] — выражение, содержащее x. \\
  Тогда $\lambda$ x. M обозначает функцию x $\to$ M[x], \\
  то есть каждому x сопоставляется M[x].\\			
  \end{description}
  \end{block}
\end{frame}


%\section{Теория}
\subsection{Введение в $\lambda$-исчисление}
\begin{frame}
  \begin{block}{}
  Применение и абстракция работают совместно: \\
  ($\lambda$x. x + 3) 39 = 42 \\
  \hspace*{\fill} \\
  {\color{blue}Def.} Отношение $\beta$-редукции $\to_{\beta}$ над $\Lambda$ :\\
  ($\lambda$x.M) N $\to_{\beta}$  M[x := N] \\
  {\color{blue}Пример:}\\
  ($\lambda$yz.y)($\lambda$p.p) $\to_{\beta}$ $\lambda$zp.p \\ 
  \hspace*{\fill} \\
  {\color{blue}Def.} Экспансия - операция обратная редукции\\ 
  {\color{blue}Пример:}\\
  $\lambda$zp.p $\to$ ($\lambda$yz.y)($\lambda$p.p) \\ 
  \end{block}
\end{frame}


\subsection{Теория}
\subsection{Типизация термов}
\begin{frame}
  \begin{block}{}
  {\color{blue}Переменная} — как угодно.\\
  {\color{blue}Пример:} x: $\alpha$, y: $\alpha$ \to $\beta$\\
  \end{block} 
  \begin{block}{}
  {\color{blue}Аппликация} MN: \\
  $${M: \sigma \to \tau \;\;\;\; N:\sigma}\over{(MN):\tau}$$
  {\color{blue}Пример:} x: $\alpha$, y: $\alpha$ \to $\beta$. Тогда (yx):$\beta$
  \end{block}
  \begin{block}{}
  {\color{blue}Абстракция} $\lambda$x.M: 
  $${x:\sigma \;\;\;\; M:\tau}\over{(\lambda x.M) : \sigma \to \tau}$$ \hspace*{\fill} \\
  {\color{blue}Пример:} Пусть x: $\alpha$, тогда ($\lambda$x. x) : $\alpha$ \to $\alpha$.\\
  \end{block}
\end{frame}


\subsection{Теория}
\subsection{Редукция, приписывание типа}
\begin{frame}
  \begin{block}{}
   Рассмотрим последовательностей редукций \\ 
   $M$ $\to_{\beta}$ $M^{\prime}$ $\to_{\beta}$ $M^{\prime\prime}$\\ 
   Припишем каждому терму тип: \\ 
   $M$: $\tau$ $\to_{\beta}$ $M^{\prime}$: $\tau$ $\to_{\beta}$ $M^{\prime\prime}$: $\tau$ \\
   Замечание: По теореме о продвижении при редукции тип сохраняется.
  \end{block}
  \begin{block}{}
   Вопрос: будет ли сохраняться наиболее общий тип при экспансии?
  \end{block}
\end{frame}


\subsection{Теория}
\subsection{Нумералы Чёрча}
\begin{frame}
  \begin{block}{}
  {\color{blue}Def.} Нумералы Черча\footnotemark[1]\\
  \~0 = $\lambda$s z. z \\
  \~1 = $\lambda$ s z. s z \\
  \~2 = $\lambda$ s z. s (s z) \\
  \~3 = $\lambda$ s z. s (s (s z)) \\
  \~4 = $\lambda$ s z. s (s (s (s z)))\\
  ... \\
  \end{block}
 \footnotetext[1]{Х. Барендрегт, Лямбда-исчисление, его синтаксис и семантика, \textbf{1985}}
\end{frame}


\subsection{Теория}
\subsection{Понятие наиболее общего типа}
\begin{frame}
  \begin{block}{}
  Рассмотрим нулевой нумерал Черча $\lambda$s z. z \\
  $${s: \alpha \;\;\;\; z:\beta}\over{0:\alpha \to \beta \to \beta}$$ \\
  Но с другой стороны \\
  $${s: \alpha \;\;\;\; z:\alpha}\over{0:\alpha \to \alpha \to \alpha}$$ 
  \hspace*{\fill} \\
  Однако, первый «лучше» в том смысле, что второй получается из него подстановкой типа вместо типовой переменной.\\
  \end{block}
\end{frame}

\subsection{Проблема}
\begin{frame}
  \begin{block}{}
  Припишем типы к нумералам Черча:\\
  \~0: \alpha \to \beta \to \beta \\
  \~1: (\beta \to \gamma) \to \beta \to \gamma \\
  \~2: (\beta \to \beta) \to \beta \to \beta \\
   .. \\
  \~n: (\beta \to \beta) \to \beta \to \beta \\
  Запишем разность между 2 нумералами\footnotemark[1], к примеру: \\	
  3 - 3 = 0\\	
  С одной стороны ясно что тип результата должен быть\\	
  (\beta \to \beta) \to \beta \to \beta \\	
  Но с другой стороны: \\
  \alpha \to \beta \to \beta \\ 
  \end{block}
  \footnotetext[1]{Джон Харрисон, Введение в функциональное программирование, \textbf{1996}}
\end{frame}


\section{Цель и задачи}
\begin{frame}
  \begin{block}{Цель работы}
  Исследовать эффект изменения типа при экспансии \\
  \end{block}
  \begin{block}{Задачи}
    \begin{enumerate}
     \item Реализовать систему редукции.
     \item Реализовать систему вывода типов.
     \item Определить условия, при которых имеет место эффект изменения типа.
    \end{enumerate}     
  \end{block}

\end{frame}


\section{Результаты}
\subsection{Просто типизированное $\lambda$-исчисление}
\begin{frame}
  \begin{block}{Результаты для просто типизированного $\lambda$-исчисления}
  {\color{blue}Реализованы: } 	
  \begin{itemize}
    \item Система пошаговой редукции термов.
    \item Система вывода типов на основе построения системы уравнений на типы и их решения.
  \end{itemize}
  {\color{blue} Помимо этого:}
  \begin{itemize}
    \item Алгоритмы расширены для работы со свободными переменными. 
    \item Реализована проверка что тело и типа лямбда выражения является функцией типа из типов аргументов и типа тела. \\
    \item Реализована подсистема строкового ввода-вывода термов и их типов.
  \end{itemize}
  \end{block}
\end{frame}

\subsection{System F}
\begin{frame}
  \begin{block}{Результаты для System F}
  Реализована подсистема System Fw $\subsetneq$ System F \\
  {\color{blue}Реализованы: } 	
  \begin{itemize}
    \item Система пошаговой редукции термов.(аналогично просто типизированному $\lambda$-исчислению)
    \item Система вывода типов на основе построения системы уравнений на типы и их решения.
  \end{itemize}
  {\color{blue} Помимо этого:}
  \begin{itemize}
    \item Алгоритмы расширены для работы со свободными переменными. 
    \item Реализована подсистема строкового ввода-вывода термов и их типов.  
    \item Она были расширена для работы с подсистемой ML.\footnotemark[1] 
    \item Подтверждены теоретические результаты для ML.
  \end{itemize}
  \end{block}
  \footnotetext[1]{Didier Le Botlan and Didier Rémy, Raising ML to the Power of System F, \textbf{2009}}
\end{frame}

\section{Выводы}
\subsection{Теорема}
\begin{frame}
  \begin{block}{Достаточное условие изменения изменения наиболее общего типа}
  Теорема \\
  В $\lambda$$\to$, пусть у замкнутого терма имеется редекс следующего вида 
  \begin{center}
  $\lambda$f.($\lambda$z.P)M
  \end{center}
  При этом z $\in$ FV(P). \\
  А в M имеется вхождение f в левой аппликативной позиции, т.е. fN \\
  Пусть помимо этого в P, нет подобного вхождения. \\
  Тогда при сокращении указанного терма происходит изменение наиболее общего типа.
  \end{block}
\end{frame}

\section{Заключение}
\begin{frame}
\begin{block}{}
{\large Наиболее важным достижением работы является то, что использованный нами подход позволил сформулировать, а затем формально доказать достаточное условие изменения наиболее общего типа.}

\end{block}
\end{frame}

\section{Благодарности}
\begin{frame}
\begin{center}
{\Huge Благодарю за внимание!}
\end{center}

\vspace{2em}

Благодарю: 
\begin{table}[H]
\begin{tabular}{l|l}
Д. Н. Москвин  & АУ \\
-- за ценные консультации \\
Е. Р. Кирпичев & Mirantis \\
-- за ценные дискуссии по функциональному \\
программированию & \\
\end{tabular}
\end{table}
\end{frame}

\end{document}

